es:ES, i:Id, R:({e:E| loc(e) = i} ), e:E.
(e:E. (loc(e) = i)  Dec(R(e)))
 (loc(e) = i)
 (e':E. (e' loc e  c R(e')))
 (e':E. (e' loc e  c (R(e') & (e'':E. (e' <loc e'')  e'' loc e   (R(e'')))))) 

latex

Definitions	x:A. B(x), , P  Q, x(s), x:A. B(x), A c B, e loc e' , P & Q, (e <loc e'), t  T, x. t(x), P  Q, T, True, WellFnd{i}(A;x,y.R(x;y)), {T}, P  Q, Dec(P), A, False
Lemmas	es-locl-wellfnd, es-locl wf, es-le-loc, es-loc wf, es-causl wf, not wf, es-loc-pred, es-locl-iff, es-E wf, Id wf, event system wf, es-le-self, es-le wf, es-le-not-locl, decidable assert, es-first wf, es-le-iff, squash wf, true wf, es-pred wf, es-pred-locl, es-locl transitivity1, es-le weakening